State of the art computerized components are complex and require extensive quality assurance checks. One of the commonly used techniques is formal verification in which the computerized component is modeled and is examined by a model checker. A verification query comprises a model and a property, wherein the model is to be checked whether it holds the property or there exists a behavior of the model that refutes the property. The model describes all possible behaviors of the computerized component based on inputs from the environment and calculations performed by the computerized component itself. Most components are represented by cycled models in which the state of the component may differ from one cycle to the other. It will be noted that the computerized component may be a software component, firmware component, hardware component or the like. It will be further noted that in some cases the component to be verified may be a business method, user interaction, communication protocol or any other form of activity or computation that may be expressed formally using a model.
A model checker checks that the model holds a predetermined specification property. An exemplary specification property may be that a triggered event is always handled by the component or that a certain variable is never assigned a predetermined value. The specification property may be attributed to one or more cycles, such as for example, after a flag is raised in a cycle, an alert is issued within a predetermined number of cycles. In some exemplary embodiments, the property may be any property such as safety property or liveness property, and may be provided using a Property Specification Language (PSL) formula such as AGp, indicating that Always (i.e., in each cycle), Globally (i.e. in each possible scenario), property p holds. Property p may be a property provided in temporal logic.
Model checkers may be symbolic model checkers, explicit model checkers, or the like. The model checker may utilize a Boolean Satisfiability problem (SAT) solver, and known as SAT-based model checkers, such as for example a Bounded Model Checker (BMC), Interpolant-based Transition Relation approximation, or the like. One form of SAT-based model checkers are model checkers that do not unroll the transition relation of the model. One such model checker is described in A. R. Bradley, “SAT-based model checking without unrolling,” in Verification, Model Checking, and Abstract Interpretation (VMCAI′ 11), 2011, pp. 70-87 (hereinafter: “Bradley”), which is hereby incorporated by reference. Additionally or alternatively, model checkers may be Binary Decision Diagrams (BDD)-based model checker.
Some model checkers are adapted to generate invariants of the model useful for the verification that the property is held. Invariants, also referred to as invars, may be useful in gaining a speed-up in model checking, enabling model checking of a previously unfeasible verification query. Invars may or may not be property-directed.